THE_GOAL_ (FIB X3 N)_IS_ATTAINABLE_BY_THE_FOLLOWING_PROGRAM:


PROC1 (X3 N)
   BEGIN
   X1 ← 2;
   X2 ← 1;
   X3 ← (1+1);
   Y1 ← 2;
   Y2 ← 1;
   Y3 ← (1+1);
   WHILE ¬>(Y1,N) DO 
      BEGIN
      Z1 ← (Y1+1);
      Z2 ← Y3;
      Z3 ← (Y3+Y2);
      X1 ← Z1;
      X2 ← Z2;
      X3 ← Z3;
      Y1 ← Z1;
      Y2 ← Z2;
      Y3 ← Z3;
      END
   END


27 __RULES_ENTERED
26 __RULES_SUCCESSFUL